abstract sig User{
}

sig Employee extends User{
Created: set BasePackage,
Added: set BasicProduct
}

abstract sig Customer extends User{
}

sig Registered extends Customer{
Saved: set SavedPackage,
Confirmed: set SavedPackage,
}

sig Unregistered extends Customer{
}

abstract sig BasicProduct{
}
sig Fly extends BasicProduct{
}
sig Hotel extends BasicProduct{
}
sig Excursion extends BasicProduct{
}

abstract sig Package{
Departure: lone Fly,
Return: lone Fly,
Books: lone Hotel,
Excursions: some Excursion,
}

sig BasePackage extends Package{
}

sig SavedPackage extends Package{
PayedBy: set Customer
}

fact NoMultipleOwners{
all sp:SavedPackage| all disj r1, r2:Registered| !((sp in r1.Saved)&&(sp in r2.Saved))
}

fact NoLoneSP{
all sp:SavedPackage| one r:Registered| sp in r.Saved
}

fact CanConfirmOnlyMySavedPackages{
all p: SavedPackage|all r: Registered| p in r.Confirmed => p in r.Saved
}

fact CanBePayedOnlyIfConfirmed{
all p: SavedPackage|some r:Registered| (some p.PayedBy)=>p in r.Confirmed 
}

fact FlyPartenzaDifferentFromDestination{
all p:Package|  p.Departure!=p.Return
}

fact EveryBasicPackageCreatedByEmployee{
all bp:BasePackage| one e:Employee| bp in e.Created
}

fact EveryBasicProductAddedByEmployee{
all bp:BasicProduct| one e:Employee| bp in e.Added
}

assert KnownCreatorBPA {
no bpa:BasePackage|all e:Employee|!(bpa in e.Created)
}
check KnownCreatorBPA for 9

assert differentFlies{
no p:Package| p.Departure=p.Return}
check differentFlies for 9

assert KnownCreatorBPR{
no bpr:BasicProduct|all e:Employee| !(bpr in e.Added)
}
check KnownCreatorBPR for 9

assert OneCreator{
all bp:BasePackage|all disj e1,e2: Employee| !((bp in e1.Created)&&(bp in e2.Created))
}
check OneCreator for 9

assert OneAdder{
all bp:BasicProduct|all disj e1,e2: Employee| !((bp in e1.Added)&&(bp in e2.Added))
}
check OneAdder for 9

assert NoPayedAndNotConfirmed{
no p:SavedPackage|all r:Registered|  (some p.PayedBy) &&!(p in r.Confirmed)
}
check NoPayedAndNotConfirmed for 9

assert AllConfirmedAreSaved{
all r:Registered| no p:SavedPackage|(p in r.Confirmed) && !(p in r.Saved)
}
check AllConfirmedAreSaved for 9


//Asserts where we WANT counterexample:

assert ExistConfirmedNotPayed{
all r:Registered|all p:SavedPackage| (p in r.Confirmed)=>(some p.PayedBy)
}
check ExistConfirmedNotPayed for 3

assert ExistPackagesWithMoreExcurions{
all p:SavedPackage| #p.Excursions<3
}
check  ExistPackagesWithMoreExcurions for 4

assert PaidPackages{
all p:SavedPackage| #p.PayedBy=0
}
check PaidPackages for 3

pred show (){
#Registered=2
#Unregistered=2
#Employee=2
#Fly=3
#Hotel=3
#Excursion=3
#BasePackage=2
#SavedPackage=2
}
run show for 9
